i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x:Id, T:Type, ks:Knd List,
tr:(k:{k:Knd| (k  ks) }State(ds)Valtype(da;k)TT).
x  dom(ds)
 (A:Realizer.
 (R-Feasible(A)
 ( R-occurs(A;i;x)
 ( ds || R-ds(A;i)
 ( da || R-da(A;i)
 ( (kks. isrcv(k)  R-da(A;source(lnk(k)))(k)?Void  Valtype(da;k))
 ( (kks. k  dom(da))
 ( (k:Knd. (k  ks)  write-restricted(A;i;k))
 ( (y:Id. y  dom(ds  x : T)  read-restricted(A; i; y))
 ( R-state-var(i;ds;da;x;T;ks;tr) || A) 

latex

Definitions

b, Void, x:AB(x), P  Q, False, A, x:A. B(x), t  T, isrcv(k), Knd, Type, R-da(R;i), f(x)?z, Valtype(da;k), f || g, Id, DeclaredType(ds;x), x : v, IdDeq, f  g, f(a), x.A(x), x. t(x), State(ds), (x  l), @loc effect knd(v:T)  x := f State(ds) v , A || B, {x:A| B(x) }, P  Q, x:AB(x), P & Q, P  Q, @loc only events in L change x:T, xL.R(x), x:A. B(x), Top, R-state-var(i;ds;da;x;T;ks;tr), a:A fp B(a), type List, x  dom(f), Realizer, R-Feasible(R), R-occurs(R;i;z), R-ds(R;i), KindDeq, lnk(k), source(l), Prop, xL. P(x), write-restricted(R;i;k), read-restricted(R; i; y), b, , s = t, Unit, left+right, {T}, SQType(T), s ~ t, <a,b>, x:A. B(x), if b t else f fi

Lemmas

and functionality wrt iff, fpf-single-dom, Knd sq, fpf-compatible-join2, fpf-compatible-single2, dom-R-ds-occurs, subtype rel dep function, fpf-cap-join-subtype, fpf-join-cap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, fpf-cap-single1, subtype rel self, top wf, read-restricted wf, write-restricted wf, l all wf, subtype rel wf, fpf-cap wf, lsrc wf, lnk wf, Kind-deq wf, R-da wf, fpf-compatible wf, R-ds wf, R-occurs wf, R-Feasible wf, es realizer wf, not wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, R-compat-Rplus-sq, R-compat-Rall2, Reffect wf, l member wf, Knd wf, not-R-occurs-frame-compat, not-R-occurs-effect-compat, ma-valtype wf, decl-state wf, fpf-join wf, fpf-single wf, Id wf, id-deq wf, assert wf, isrcv wf